g:GrpSig{i}. NormSubGrp{i}(g)  Type{i'} 

latex

Up	groups 1
Definitions of Statement	NormSubGrp{i}(g)
Definitions	P & Q, , NormSubGrp{i}(g), t  T, x:A. B(x)
Lemmas	grp sig wf, norm subset p wf, subgrp p wf, grp car wf